<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>Untyped | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/Tutorials/">
              <span property="name"><b>Tutorials</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">Untyped</span>
            <meta property="position" content="3" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    

<div class="sidebar">
  <ul class="nav nav-sidebar tutorial-sidebar">
    <li class="nav-section">Getting started</li>
      <li><a href="/Tutorials/">Overview</a></li>
      <li><a href="/Tutorials/pathways">Tutorial pathways</a></li>
    <li class="nav-section">seL4</li>
      <li><a href="/Tutorials/setting-up">Setting up your machine</a></li>
      <li><a href="/Tutorials/get-the-tutorials">Getting the tutorials</a></li>
      <li><a href="/Tutorials/hello-world">Hello world</a></li>
      <li><a href="/Tutorials/capabilities">Capabilities</a></li>
      <li><a href="/Tutorials/untyped">Untyped</a></li>
      <li><a href="/Tutorials/mapping">Mapping</a></li>
      <li><a href="/Tutorials/threads">Threads</a></li>
      <li><a href="/Tutorials/ipc">IPC</a></li>
      <li><a href="/Tutorials/notifications">Notifications</a></li>
      <li><a href="/Tutorials/interrupts">Interrupts</a></li>
      <li><a href="/Tutorials/fault-handlers">Fault handling</a></li>
      <li><a href="/Tutorials/mcs">MCS extensions</a></li>
    <li class="nav-section">C Libraries</li>
      <li><a href="/Tutorials/libraries-1">Initialisation &amp; threading</a></li>
      <li><a href="/Tutorials/libraries-2">IPC</a></li>
      <li><a href="/Tutorials/libraries-3">Processes &amp; Elf loading</a></li>
      <li><a href="/Tutorials/libraries-4">Timer</a></li>
    <li class="nav-section">Microkit</li>
      <li><a href="https://trustworthy.systems/projects/microkit/tutorial/">Tutorial</a></li>
    <li class="nav-section">CAmkES</li>
      <li><a href="/Tutorials/hello-camkes-0">Hello CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-1">Introduction to CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-2">Events in CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-timer">CAmkES timer tutorial</a></li>
      <li><a href="/Tutorials/camkes-vm-linux">CAmkES VM</a></li>
      <li><a href="/Tutorials/camkes-vm-crossvm">CAmkES cross-VM connectors</a></li>
    <li class="nav-section">Rust</li>
      <li><a href="https://github.com/seL4/rust-sel4">GitHub</a></li>
    <li class="nav-section">Resources</li>
      <li><a href="https://sel4.systems/Info/Docs/seL4-manual-latest.pdf">seL4 Manual</a></li>
      <li><a href="/projects/sel4/api-doc.html">seL4 API reference</a></li>
      <li><a href="/Tutorials/how-to">How to: a quick solutions guide</a></li>
      <li><a href="/projects/sel4-tutorials/debugging-guide">Debugging guide</a></li>
      <li><a href="/Resources#contact">Help contacts</a></li>
  </ul>
</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">

    
<!--
  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)

  SPDX-License-Identifier: BSD-2-Clause
-->

<h1 id="untyped">Untyped</h1>

<p>This tutorial provides an introduction to physical memory management on seL4.</p>

<p>It covers:</p>
<ol>
  <li>The jargon <em>untyped</em>, <em>device untyped</em>, and <em>bit size</em>.</li>
  <li>How to create objects from untyped memory in seL4.</li>
  <li>How to reclaim objects.</li>
</ol>

<h2 id="prerequisites">Prerequisites</h2>

<ol>
  <li><a href="/Tutorials/setting-up">Set up your machine</a></li>
  <li><a href="/Tutorials/capabilities">Capabilities tutorial</a></li>
</ol>

<h2 id="initialising">Initialising</h2>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--tut</span> untyped
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>untyped_build
ninja
</code></pre></div></div>

<details>
  <summary><em>Hint:</em> tutorial solutions</summary>
  <p><br />
All tutorials come with complete solutions. To get solutions run:</p>

  <div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--solution</span> <span class="nt">--tut</span> untyped
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>untyped_build
ninja
</code></pre></div>  </div>

  <p>Answers are also available in drop down menus under each section.</p>
</details>

<h2 id="background">Background</h2>

<h3 id="physical-memory">Physical memory</h3>

<p>Apart from a small, static amount of kernel memory, all physical memory is managed by user level in an seL4
system. Capabilities to objects created by seL4 at boot, as well as the rest of the physical resources managed by seL4,
are passed to the root task on start up.</p>

<h3 id="untyped-memory-and-capabilities">Untyped memory and capabilities</h3>

<p>Excluding the objects used to create the root task, capabilities to all
available physical memory are passed to the root task as capabilities to
<em>untyped</em> memory. Untyped memory is a block of contiguous physical memory with a
specific size. Untyped capabilities are capabilities to untyped memory. Untyped
capabilities can be <em>retyped</em> into kernel objects together with capabilities to
them, or into further, usually smaller, untyped capabilities.</p>

<p>Untyped capabilities have a boolean property <em>device</em> which indicates whether
the memory is writable by the kernel or not: it may not be backed by RAM but
some other device, or it may be in an area of RAM not addressable by the kernel.
Device untyped capabilities can only be retyped intro frame objects (physical
memory frames, which can be mapped into virtual memory), and cannot be written
to by the kernel.</p>

<h3 id="initial-state">Initial state</h3>

<p>The <code class="language-plaintext highlighter-rouge">seL4_BootInfo</code> structure provided to the root task describes all of the untyped capabilities, including their size,
if they are a device untyped, and the physical address of the untyped. The code example below
shows how to print out the initial untyped capabilities provided from <code class="language-plaintext highlighter-rouge">seL4_BootInfo</code>.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">printf</span><span class="p">(</span><span class="s">"    CSlot   </span><span class="se">\t</span><span class="s">Paddr           </span><span class="se">\t</span><span class="s">Size</span><span class="se">\t</span><span class="s">Type</span><span class="se">\n</span><span class="s">"</span><span class="p">);</span>
    <span class="k">for</span> <span class="p">(</span><span class="n">seL4_CPtr</span> <span class="n">slot</span> <span class="o">=</span> <span class="n">info</span><span class="o">-&gt;</span><span class="n">untyped</span><span class="p">.</span><span class="n">start</span><span class="p">;</span> <span class="n">slot</span> <span class="o">!=</span> <span class="n">info</span><span class="o">-&gt;</span><span class="n">untyped</span><span class="p">.</span><span class="n">end</span><span class="p">;</span> <span class="n">slot</span><span class="o">++</span><span class="p">)</span> <span class="p">{</span>
        <span class="n">seL4_UntypedDesc</span> <span class="o">*</span><span class="n">desc</span> <span class="o">=</span> <span class="o">&amp;</span><span class="n">info</span><span class="o">-&gt;</span><span class="n">untypedList</span><span class="p">[</span><span class="n">slot</span> <span class="o">-</span> <span class="n">info</span><span class="o">-&gt;</span><span class="n">untyped</span><span class="p">.</span><span class="n">start</span><span class="p">];</span>
        <span class="n">printf</span><span class="p">(</span><span class="s">"%8p</span><span class="se">\t</span><span class="s">%16p</span><span class="se">\t</span><span class="s">2^%d</span><span class="se">\t</span><span class="s">%s</span><span class="se">\n</span><span class="s">"</span><span class="p">,</span> <span class="p">(</span><span class="kt">void</span> <span class="o">*</span><span class="p">)</span> <span class="n">slot</span><span class="p">,</span> <span class="p">(</span><span class="kt">void</span> <span class="o">*</span><span class="p">)</span> <span class="n">desc</span><span class="o">-&gt;</span><span class="n">paddr</span><span class="p">,</span> <span class="n">desc</span><span class="o">-&gt;</span><span class="n">sizeBits</span><span class="p">,</span> <span class="n">desc</span><span class="o">-&gt;</span><span class="n">isDevice</span> <span class="o">?</span> <span class="s">"device untyped"</span> <span class="o">:</span> <span class="s">"untyped"</span><span class="p">);</span>
    <span class="p">}</span>
</code></pre></div></div>

<h3 id="retyping">Retyping</h3>

<p>Untyped capabilities have a single invocation:
<a href="https://docs.sel4.systems/ApiDoc.html#retype">seL4_Untyped_Retype</a> which is
used to create a new capability (and potentially object) from an untyped
capability. Specifically, the new capability created by a retype invocation
provides access to a subset of the memory range of the original capability,
either as a smaller untyped capability, or pointing to a new object with a
specific type. New capabilities created by retyping an untyped capability are
referred to as <em>children</em> of that untyped capability.</p>

<p>Untyped capabilities are retyped incrementally in a greedy fashion from the
invoked untyped, which is important to understand in order to gain efficient
memory utilisation in seL4 systems. Each untyped capability maintains a single
watermark, with addresses before the watermark being unavailable (already
retyped) and after the watermark being free (not retyped yet). On a retype
operation, the watermark is moved first to the alignment of the object being
created, and then to the end of the size of the object. For example, if we
create first a 4KiB object and then a 16KiB object, the 12KiB between the end of
the 4KiB object and the start of the 16KiB object are wasted due to alignment.
The memory cannot be reclaimed until both children are revoked.</p>

<p>TL;DR: objects should be allocated in order of size, largest first, to avoid wasting memory.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_Untyped_Retype</span><span class="p">(</span><span class="n">parent_untyped</span><span class="p">,</span> <span class="c1">// the untyped capability to retype</span>
                                <span class="n">seL4_UntypedObject</span><span class="p">,</span> <span class="c1">// type</span>
                                <span class="n">untyped_size_bits</span><span class="p">,</span>  <span class="c1">//size</span>
                                <span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="c1">// root</span>
                                <span class="mi">0</span><span class="p">,</span> <span class="c1">// node_index</span>
                                <span class="mi">0</span><span class="p">,</span> <span class="c1">// node_depth</span>
                                <span class="n">child_untyped</span><span class="p">,</span> <span class="c1">// node_offset</span>
                                <span class="mi">1</span> <span class="c1">// num_caps</span>
                                <span class="p">);</span>
</code></pre></div></div>

<p>The above code snippet shows an example of retyping an untyped into a smaller,
4KiB untyped capability (despite the name <code class="language-plaintext highlighter-rouge">seL4_UntypedObject</code> no object is
created, the new untyped capability simply points to a subset of the untyped
memory of <code class="language-plaintext highlighter-rouge">parent_untyped</code>. However, it is convenient to treat this memory like
an object for the purposes of this operation). We will refer to this snippet as
we discuss each parameter in the retype invocation. Recall that the first
parameter is the untyped capability being invoked to do the retype.</p>

<h4 id="types">Types</h4>

<p>Each object in seL4 has a specific type, and all of the type constants can be found in <code class="language-plaintext highlighter-rouge">libsel4</code>. Some types
are architecture specific, while others are general across architectures. In the example above, we create a
new untyped capability, which can be further retyped. All other object type parameters create kernel objects <em>and</em>
capabilities to them, and the type of the created object (and capability) determines the invocations
that can be made on that capability. For example, were we to retype into a thread control block
(TCB – <code class="language-plaintext highlighter-rouge">seL4_TCBObject</code>), we could then perform TCB invocations on the capability to the new TCB object, including <code class="language-plaintext highlighter-rouge">seL4_TCB_SetPriority</code>.</p>

<h4 id="size">Size</h4>

<p>The size argument determines the size of the new object. The meaning of the argument
depends on the object type that is being requested:</p>

<ul>
  <li>most objects in seL4 are fixed size, and for these, the kernel will <em>ignore</em>
the size argument;</li>
  <li>the types <code class="language-plaintext highlighter-rouge">seL4_UntypedObject</code> and <code class="language-plaintext highlighter-rouge">seL4_SchedContextObject</code> allow a
variable size, which is specified in <code class="language-plaintext highlighter-rouge">size_bits</code> (more below);</li>
  <li>the type <code class="language-plaintext highlighter-rouge">seL4_CapTableObject</code> is also of variable size, and the argument specifies
the <em>number of capability slots</em>. The same mechanism as for <code class="language-plaintext highlighter-rouge">size_bits</code> is used,
but for the number of slots, not the size in bytes.</li>
</ul>

<p>In general in seL4, if sizes are measured in bits, they are powers
of two. “Bits”  does not refer to the number of bits the object takes up, but
the bit-width that is needed to describe its contents. An object of bit size <code class="language-plaintext highlighter-rouge">n</code>
measures 2<sup><code class="language-plaintext highlighter-rouge">n</code></sup> bytes. Also, generally in seL4, objects and memory
regions are aligned to their size, i.e. an <code class="language-plaintext highlighter-rouge">n</code>-bit object is aligned to
2<sup><code class="language-plaintext highlighter-rouge">n</code></sup> bytes, or, equivalently, the address of the object has 0 as its
<code class="language-plaintext highlighter-rouge">n</code> bottom bits.</p>

<p>For <code class="language-plaintext highlighter-rouge">retype</code>, it is enough to remember that the parameter <code class="language-plaintext highlighter-rouge">size_bits</code> means the
object will measure 2<sup><code class="language-plaintext highlighter-rouge">size_bits</code></sup> bytes, and for <code class="language-plaintext highlighter-rouge">seL4_CapTableObject</code>
that you are requesting 2<sup><code class="language-plaintext highlighter-rouge">size_bits</code></sup> slots (you can compute the size
in bytes by taking 2<sup><code class="language-plaintext highlighter-rouge">size_bits + seL4_SlotBits</code></sup>).</p>

<h4 id="root-node_index--node_depth">Root, node_index &amp; node_depth</h4>

<p>The <code class="language-plaintext highlighter-rouge">root</code>, <code class="language-plaintext highlighter-rouge">node_index</code> and <code class="language-plaintext highlighter-rouge">node_depth</code> parameters are used to specify the CNode in which to place the new capabilities.
Depending on the <code class="language-plaintext highlighter-rouge">depth</code> parameter, the CSlot to use is addressed by invocation or by direct addressing (see the <a href="/Tutorials/capabilities.html">capabilities tutorial</a> for an explanation of those terms).</p>

<p>In the example above, <code class="language-plaintext highlighter-rouge">node_depth</code> is set to 0, which means invocation addressing is used: the <code class="language-plaintext highlighter-rouge">root</code> parameter is
looked up implicitly using the CSpace root of the current thread at a depth of <code class="language-plaintext highlighter-rouge">seL4_WordBits</code>. So the example code
specifies the root task’s CNode (<code class="language-plaintext highlighter-rouge">seL4_CapInitThreadCNode</code>). The <code class="language-plaintext highlighter-rouge">node_index</code> parameter in this case is ignored.</p>

<p>If the <code class="language-plaintext highlighter-rouge">node_depth</code> value is not set to 0, then direct addressing is used with the current thread’s CSpace root
as the root. Then the <code class="language-plaintext highlighter-rouge">node_index</code> parameter is used to locate the CNode capability to place new capabilities in,
at the specified <code class="language-plaintext highlighter-rouge">node_depth</code>. This is designed for managing multi-level CSpaces, and is not covered in this tutorial.</p>

<h4 id="node_offset">Node_offset</h4>

<p>The node_offset is the CSlot to start creating new capabilities at, in the CNode selected by the previous parameters.
 In this case, the first empty CSlot in the initial CNode is selected.</p>

<h4 id="num_caps">Num_caps</h4>

<p>The retype invocation can be used to create more than 1 capability and object at a time – the number of capabilities is
specified using this argument. Note that there are two constraints on this value:</p>

<ol>
  <li>The untyped must be big enough to fit all of the memory being retyped (<code class="language-plaintext highlighter-rouge">num_caps * (1u &lt;&lt; size_bits)</code>).</li>
  <li>The CNode must have enough consecutive free CSlots to fit all of the new capabilities.</li>
</ol>

<h2 id="exercises">Exercises</h2>

<h3 id="create-an-untyped-capability">Create an untyped capability</h3>

<p>When you first run this tutorial, you will see something like the following output, which lists all of the
untyped capabilities provided to the root task on boot:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Booting all finished, dropped to user space
    CSlot   Paddr       Size    Type
   0x12d    0x100000    2^20    device untyped
   0x12e    0x200000    2^21    device untyped
   0x12f    0x400000    2^22    device untyped
   0x130    0xb2e000    2^13    device untyped
</code></pre></div></div>

<p>At the end of the output, there is an error:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>&lt;&lt;seL4(CPU 0) [decodeUntypedInvocation/105 T0xffffff801ffb5400 "rootserver" @4012e1]: Untyped Retype: Requested UntypedItem size too small.&gt;&gt;
main@main.c:49 [Cond failed: error != seL4_NoError]
    Failed to retype
</code></pre></div></div>

<p>This error happens because we are trying to create an untyped of size 0.</p>

<p><strong>Exercise</strong> Calculate the size of the child untyped required, such that the child untyped can be used
 to create all of the objects listed in the <code class="language-plaintext highlighter-rouge">objects</code> array. Remember that object sizes are measured in
 bits, that is, in powers of two.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// list of general seL4 objects</span>
    <span class="n">seL4_Word</span> <span class="n">objects</span><span class="p">[]</span> <span class="o">=</span> <span class="p">{</span><span class="n">seL4_TCBObject</span><span class="p">,</span> <span class="n">seL4_EndpointObject</span><span class="p">,</span> <span class="n">seL4_NotificationObject</span><span class="p">};</span>
    <span class="c1">// list of general seL4 object size_bits</span>
    <span class="n">seL4_Word</span> <span class="n">sizes</span><span class="p">[]</span> <span class="o">=</span> <span class="p">{</span><span class="n">seL4_TCBBits</span><span class="p">,</span> <span class="n">seL4_EndpointBits</span><span class="p">,</span> <span class="n">seL4_NotificationBits</span><span class="p">};</span>

    <span class="c1">// TODO work out what size object we need to create to be able to create all of the objects</span>
    <span class="c1">// listed above. Remember that sizes are in bits, that is, the exponents of powers of two.</span>
    <span class="n">seL4_Word</span> <span class="n">untyped_size_bits</span> <span class="o">=</span> <span class="mi">0</span><span class="p">;</span>
    <span class="n">seL4_CPtr</span> <span class="n">parent_untyped</span> <span class="o">=</span> <span class="mi">0</span><span class="p">;</span>
    <span class="n">seL4_CPtr</span> <span class="n">child_untyped</span> <span class="o">=</span> <span class="n">info</span><span class="o">-&gt;</span><span class="n">empty</span><span class="p">.</span><span class="n">start</span><span class="p">;</span>

    <span class="c1">// First, find an untyped big enough to fit all of our objects</span>
    <span class="k">for</span> <span class="p">(</span><span class="kt">int</span> <span class="n">i</span> <span class="o">=</span> <span class="mi">0</span><span class="p">;</span> <span class="n">i</span> <span class="o">&lt;</span> <span class="p">(</span><span class="n">info</span><span class="o">-&gt;</span><span class="n">untyped</span><span class="p">.</span><span class="n">end</span> <span class="o">-</span> <span class="n">info</span><span class="o">-&gt;</span><span class="n">untyped</span><span class="p">.</span><span class="n">start</span><span class="p">);</span> <span class="n">i</span><span class="o">++</span><span class="p">)</span> <span class="p">{</span>
        <span class="k">if</span> <span class="p">(</span><span class="n">info</span><span class="o">-&gt;</span><span class="n">untypedList</span><span class="p">[</span><span class="n">i</span><span class="p">].</span><span class="n">sizeBits</span> <span class="o">&gt;=</span> <span class="n">untyped_size_bits</span> <span class="o">&amp;&amp;</span> <span class="o">!</span><span class="n">info</span><span class="o">-&gt;</span><span class="n">untypedList</span><span class="p">[</span><span class="n">i</span><span class="p">].</span><span class="n">isDevice</span><span class="p">)</span> <span class="p">{</span>
            <span class="n">parent_untyped</span> <span class="o">=</span> <span class="n">info</span><span class="o">-&gt;</span><span class="n">untyped</span><span class="p">.</span><span class="n">start</span> <span class="o">+</span> <span class="n">i</span><span class="p">;</span>
            <span class="k">break</span><span class="p">;</span>
        <span class="p">}</span>
    <span class="p">}</span>

</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// list of general seL4 objects</span>
    <span class="n">seL4_Word</span> <span class="n">objects</span><span class="p">[]</span> <span class="o">=</span> <span class="p">{</span><span class="n">seL4_TCBObject</span><span class="p">,</span> <span class="n">seL4_EndpointObject</span><span class="p">,</span> <span class="n">seL4_NotificationObject</span><span class="p">};</span>
    <span class="c1">// list of general seL4 object size_bits</span>
    <span class="n">seL4_Word</span> <span class="n">sizes</span><span class="p">[]</span> <span class="o">=</span> <span class="p">{</span><span class="n">seL4_TCBBits</span><span class="p">,</span> <span class="n">seL4_EndpointBits</span><span class="p">,</span> <span class="n">seL4_NotificationBits</span><span class="p">};</span>

    <span class="c1">// seL4_EndpointBits and seL4_NotificationBits are both less than seL4_TCBBits, which</span>
    <span class="c1">// means that all objects together fit into the size of two TCBs, or 2^(seL4_TCBBits + 1):</span>
    <span class="n">seL4_Word</span> <span class="n">untyped_size_bits</span> <span class="o">=</span> <span class="n">seL4_TCBBits</span> <span class="o">+</span> <span class="mi">1</span><span class="p">;</span>
    <span class="n">seL4_CPtr</span> <span class="n">parent_untyped</span> <span class="o">=</span> <span class="mi">0</span><span class="p">;</span>
    <span class="n">seL4_CPtr</span> <span class="n">child_untyped</span> <span class="o">=</span> <span class="n">info</span><span class="o">-&gt;</span><span class="n">empty</span><span class="p">.</span><span class="n">start</span><span class="p">;</span>

    <span class="c1">// First, find an untyped big enough to fit all of our objects</span>
    <span class="k">for</span> <span class="p">(</span><span class="kt">int</span> <span class="n">i</span> <span class="o">=</span> <span class="mi">0</span><span class="p">;</span> <span class="n">i</span> <span class="o">&lt;</span> <span class="p">(</span><span class="n">info</span><span class="o">-&gt;</span><span class="n">untyped</span><span class="p">.</span><span class="n">end</span> <span class="o">-</span> <span class="n">info</span><span class="o">-&gt;</span><span class="n">untyped</span><span class="p">.</span><span class="n">start</span><span class="p">);</span> <span class="n">i</span><span class="o">++</span><span class="p">)</span> <span class="p">{</span>
        <span class="k">if</span> <span class="p">(</span><span class="n">info</span><span class="o">-&gt;</span><span class="n">untypedList</span><span class="p">[</span><span class="n">i</span><span class="p">].</span><span class="n">sizeBits</span> <span class="o">&gt;=</span> <span class="n">untyped_size_bits</span> <span class="o">&amp;&amp;</span> <span class="o">!</span><span class="n">info</span><span class="o">-&gt;</span><span class="n">untypedList</span><span class="p">[</span><span class="n">i</span><span class="p">].</span><span class="n">isDevice</span><span class="p">)</span> <span class="p">{</span>
            <span class="n">parent_untyped</span> <span class="o">=</span> <span class="n">info</span><span class="o">-&gt;</span><span class="n">untyped</span><span class="p">.</span><span class="n">start</span> <span class="o">+</span> <span class="n">i</span><span class="p">;</span>
            <span class="k">break</span><span class="p">;</span>
        <span class="p">}</span>
    <span class="p">}</span>
</code></pre></div>  </div>

</details>

<p>On success, the tutorial will progress further, printing “Failed to set priority”</p>

<h3 id="create-a-tcb-object">Create a TCB Object</h3>

<p>The priority check is failing as <code class="language-plaintext highlighter-rouge">child_tcb</code> is an empty CSlot.</p>

<p><strong>Exercise</strong> fix this by creating a TCB object from <code class="language-plaintext highlighter-rouge">child_untyped</code> and place its cap into the <code class="language-plaintext highlighter-rouge">child_tcb</code> CSlot.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// use the slot after child_untyped for the new TCB cap:</span>
    <span class="n">seL4_CPtr</span> <span class="n">child_tcb</span> <span class="o">=</span> <span class="n">child_untyped</span> <span class="o">+</span> <span class="mi">1</span><span class="p">;</span>
    <span class="cm">/* TODO create a TCB in CSlot child_tcb */</span>

    <span class="c1">// try to set the TCB priority</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_TCB_SetPriority</span><span class="p">(</span><span class="n">child_tcb</span><span class="p">,</span> <span class="n">seL4_CapInitThreadTCB</span><span class="p">,</span> <span class="mi">10</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_NoError</span><span class="p">,</span> <span class="s">"Failed to set priority"</span><span class="p">);</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// use the slot after child_untyped for the new TCB cap:</span>
    <span class="n">seL4_CPtr</span> <span class="n">child_tcb</span> <span class="o">=</span> <span class="n">child_untyped</span> <span class="o">+</span> <span class="mi">1</span><span class="p">;</span>
    <span class="n">seL4_Untyped_Retype</span><span class="p">(</span><span class="n">child_untyped</span><span class="p">,</span> <span class="n">seL4_TCBObject</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="n">child_tcb</span><span class="p">,</span> <span class="mi">1</span><span class="p">);</span>

    <span class="c1">// try to set the TCB priority</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_TCB_SetPriority</span><span class="p">(</span><span class="n">child_tcb</span><span class="p">,</span> <span class="n">seL4_CapInitThreadTCB</span><span class="p">,</span> <span class="mi">10</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_NoError</span><span class="p">,</span> <span class="s">"Failed to set priority"</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On success, the tutorial will progress further, printing “Endpoint cap is null cap”.</p>

<h3 id="create-an-endpoint-object">Create an endpoint object</h3>

<p>The error you see now is caused be an invalid endpoint capability.</p>

<p><strong>Exercise</strong> Create an endpoint object from <code class="language-plaintext highlighter-rouge">child_untyped</code> and place its cap into the <code class="language-plaintext highlighter-rouge">child_ep</code> CSlot.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// use the slot after child_tcb for the new endpoint cap:</span>
    <span class="n">seL4_CPtr</span> <span class="n">child_ep</span> <span class="o">=</span> <span class="n">child_tcb</span> <span class="o">+</span> <span class="mi">1</span><span class="p">;</span>
    <span class="cm">/* TODO create an endpoint in CSlot child_ep */</span>

    <span class="c1">// identify the type of child_ep</span>
    <span class="kt">uint32_t</span> <span class="n">cap_id</span> <span class="o">=</span> <span class="n">seL4_DebugCapIdentify</span><span class="p">(</span><span class="n">child_ep</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">cap_id</span> <span class="o">==</span> <span class="mi">0</span><span class="p">,</span> <span class="s">"Endpoint cap is null cap"</span><span class="p">);</span>

</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// use the slot after child_tcb for the new endpoint cap:</span>
    <span class="n">seL4_CPtr</span> <span class="n">child_ep</span> <span class="o">=</span> <span class="n">child_tcb</span> <span class="o">+</span> <span class="mi">1</span><span class="p">;</span>
    <span class="n">seL4_Untyped_Retype</span><span class="p">(</span><span class="n">child_untyped</span><span class="p">,</span> <span class="n">seL4_EndpointObject</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="n">child_ep</span><span class="p">,</span> <span class="mi">1</span><span class="p">);</span>

    <span class="c1">// identify the type of child_ep</span>
    <span class="kt">uint32_t</span> <span class="n">cap_id</span> <span class="o">=</span> <span class="n">seL4_DebugCapIdentify</span><span class="p">(</span><span class="n">child_ep</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">cap_id</span> <span class="o">==</span> <span class="mi">0</span><span class="p">,</span> <span class="s">"Endpoint cap is null cap"</span><span class="p">);</span>
</code></pre></div>  </div>

</details>

<p>On success, the output will be “Failed to bind notification.”</p>

<h3 id="create-a-notification-object">Create a notification object</h3>

<p>The next part of the tutorial attempts to use a notification object that does not yet exist.</p>

<p><strong>Exercise</strong> create a notification object from <code class="language-plaintext highlighter-rouge">child_untyped</code> and place its cap into the <code class="language-plaintext highlighter-rouge">child_ntfn</code> CSlot.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// use the slot after child_ep for the new notification cap:</span>
    <span class="n">seL4_CPtr</span> <span class="n">child_ntfn</span> <span class="o">=</span> <span class="n">child_ep</span> <span class="o">+</span> <span class="mi">1</span><span class="p">;</span>
    <span class="c1">// TODO create a notification object in CSlot child_ntfn</span>

    <span class="c1">// try to use child_ntfn</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_TCB_BindNotification</span><span class="p">(</span><span class="n">child_tcb</span><span class="p">,</span> <span class="n">child_ntfn</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_NoError</span><span class="p">,</span> <span class="s">"Failed to bind notification."</span><span class="p">);</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// use the slot after child_ep for the new notification cap:</span>
    <span class="n">seL4_CPtr</span> <span class="n">child_ntfn</span> <span class="o">=</span> <span class="n">child_ep</span> <span class="o">+</span> <span class="mi">1</span><span class="p">;</span>
    <span class="n">seL4_Untyped_Retype</span><span class="p">(</span><span class="n">child_untyped</span><span class="p">,</span> <span class="n">seL4_NotificationObject</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="n">child_ntfn</span><span class="p">,</span> <span class="mi">1</span><span class="p">);</span>

    <span class="c1">// try to use child_ntfn</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_TCB_BindNotification</span><span class="p">(</span><span class="n">child_tcb</span><span class="p">,</span> <span class="n">child_ntfn</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_NoError</span><span class="p">,</span> <span class="s">"Failed to bind notification."</span><span class="p">);</span>
</code></pre></div>  </div>

</details>

<p>On success, the output will be “Failed to create endpoints.”</p>

<h3 id="delete-the-objects">Delete the objects</h3>

<p>The final part of the tutorial attempts to create enough endpoint objects from <code class="language-plaintext highlighter-rouge">child_untyped</code> to consume the
entire untyped object. However, this fails, because the untyped is already completely consumed by the previous allocations.</p>

<p><strong>Exercise</strong> revoke the child untyped, so we can create new objects from it that use up the whole thing.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// TODO revoke the child untyped</span>

    <span class="c1">// allocate the whole child_untyped as endpoints</span>
    <span class="c1">// Remember the sizes are exponents, so this computes 2^untyped_size_bits / 2^seL4_EndpointBits:</span>
    <span class="n">seL4_Word</span> <span class="n">num_eps</span> <span class="o">=</span> <span class="n">BIT</span><span class="p">(</span><span class="n">untyped_size_bits</span> <span class="o">-</span> <span class="n">seL4_EndpointBits</span><span class="p">);</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_Untyped_Retype</span><span class="p">(</span><span class="n">child_untyped</span><span class="p">,</span> <span class="n">seL4_EndpointObject</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="n">child_tcb</span><span class="p">,</span> <span class="n">num_eps</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_NoError</span><span class="p">,</span> <span class="s">"Failed to create endpoints."</span><span class="p">);</span>

    <span class="n">printf</span><span class="p">(</span><span class="s">"Success</span><span class="se">\n</span><span class="s">"</span><span class="p">);</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_CNode_Revoke</span><span class="p">(</span><span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">child_untyped</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">);</span>
    <span class="n">assert</span><span class="p">(</span><span class="n">error</span> <span class="o">==</span> <span class="n">seL4_NoError</span><span class="p">);</span>

    <span class="c1">// allocate the whole child_untyped as endpoints</span>
    <span class="c1">// Remember the sizes are exponents, so this computes 2^untyped_size_bits / 2^seL4_EndpointBits:</span>
    <span class="n">seL4_Word</span> <span class="n">num_eps</span> <span class="o">=</span> <span class="n">BIT</span><span class="p">(</span><span class="n">untyped_size_bits</span> <span class="o">-</span> <span class="n">seL4_EndpointBits</span><span class="p">);</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_Untyped_Retype</span><span class="p">(</span><span class="n">child_untyped</span><span class="p">,</span> <span class="n">seL4_EndpointObject</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="n">child_tcb</span><span class="p">,</span> <span class="n">num_eps</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_NoError</span><span class="p">,</span> <span class="s">"Failed to create endpoints."</span><span class="p">);</span>

    <span class="n">printf</span><span class="p">(</span><span class="s">"Success</span><span class="se">\n</span><span class="s">"</span><span class="p">);</span>
</code></pre></div>  </div>

</details>

<p>Once the tutorial is completed successfully, you should see the message “Success.”</p>

<h3 id="further-exercises">Further exercises</h3>

<p>That’s all for the detailed content of this tutorial. Below we list other ideas for exercises you can try
to become more familiar with untyped objects and memory allocation in seL4.</p>

<ul>
  <li>Allocate objects at specific physical addresses.</li>
  <li>Create a simple object allocator for allocating seL4 objects.</li>
</ul>



<p style="text-align: right;">

      Next: <a href="/Tutorials/mapping">Mapping</a>
</p>

<hr>
    <p><em>Tutorial included from <a href="https://github.com/sel4/sel4-tutorials/blob/master/tutorials/untyped/untyped.md">github repo</a> <a href="https://github.com/sel4/sel4-tutorials/edit/master/tutorials/untyped/untyped.md">edit</a></em></p>
  </div>

  
    
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
    <ul id="toc" class="section-nav">
<li class="toc-entry toc-h2"><a href="#prerequisites">Prerequisites</a></li>
<li class="toc-entry toc-h2"><a href="#initialising">Initialising</a></li>
<li class="toc-entry toc-h2"><a href="#background">Background</a>
<ul>
<li class="toc-entry toc-h3"><a href="#physical-memory">Physical memory</a></li>
<li class="toc-entry toc-h3"><a href="#untyped-memory-and-capabilities">Untyped memory and capabilities</a></li>
<li class="toc-entry toc-h3"><a href="#initial-state">Initial state</a></li>
<li class="toc-entry toc-h3"><a href="#retyping">Retyping</a>
<ul>
<li class="toc-entry toc-h4"><a href="#types">Types</a></li>
<li class="toc-entry toc-h4"><a href="#size">Size</a></li>
<li class="toc-entry toc-h4"><a href="#root-node_index--node_depth">Root, node_index &amp; node_depth</a></li>
<li class="toc-entry toc-h4"><a href="#node_offset">Node_offset</a></li>
<li class="toc-entry toc-h4"><a href="#num_caps">Num_caps</a></li>
</ul>
</li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#exercises">Exercises</a>
<ul>
<li class="toc-entry toc-h3"><a href="#create-an-untyped-capability">Create an untyped capability</a></li>
<li class="toc-entry toc-h3"><a href="#create-a-tcb-object">Create a TCB Object</a></li>
<li class="toc-entry toc-h3"><a href="#create-an-endpoint-object">Create an endpoint object</a></li>
<li class="toc-entry toc-h3"><a href="#create-a-notification-object">Create a notification object</a></li>
<li class="toc-entry toc-h3"><a href="#delete-the-objects">Delete the objects</a></li>
<li class="toc-entry toc-h3"><a href="#further-exercises">Further exercises</a></li>
</ul>
</li>
</ul>
</div>

  
</div>
<script src="/assets/js/toggle-markdown.js"></script>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Mon Jan 6 18:52:01 2025 +1100 df31e5ccb8
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/Tutorials/untyped.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/Tutorials/untyped.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
